Nuprl Lemma : decidable__qle
11,40
postcript
pdf
a
,
b
:
. Dec(
a
b
)
latex
Definitions
t
.2
,
t
.1
,
q_le(
r
;
s
)
,
,
x
f
y
,
<
+>
,
a
b
,
t
T
,
r
s
,
x
:
A
.
B
(
x
)
Lemmas
rationals
wf
,
qeq
wf2
,
qsub
wf
,
qpositive
wf
,
bor
wf
,
member-decide-assert
origin
a, b:
. Dec(a 
b) a, b:. Dec(a b) 
+> b
T sx:A. B(x)